#include <cstdlib>
#include <iostream>
#include <stdio.h>
#include <dirent.h>

#include "SatTask.h"
#include "SatSolver.h"

using namespace std;

int solve(const SatTask &task, vector<int> &result) {
    SatSolver solver(task);
    solver.init();
    int answer = solver.runSolutionLoop();
    if (answer) {
        result = solver.getVariables();
    }
    return answer;
}

void solve(ifstream &file) {
    if (!file) {
        cout << "No file";
        return;
    }
    SatTask task(file);

    cout << "c Start solving.\n";

    vector<int> result;

    int start = clock();

    bool isSat = solve(task, result);

    if (isSat) {
        cout << "s SATISFIABLE\n";
        cout << "v ";
        for (size_t i = 0; i < result.size(); i++) {
            cout << result[i] << " ";
        }
        cout << "\n";
        if (!task.checkResult(result)) {
            cout << " -|-|-|-|-|- Wrong answer -|-|-|-|-|- " << "\n";
        }
    } else {
        cout << "s UNSATISFIABLE\n";
    }

    int end = clock() - start;

    cout << "c Time " << (end / (CLOCKS_PER_SEC / 1000)) << "\n";

    if (isSat) {
        exit(10);
    } else {
        exit(20);
    }
}

int main(int argc, char *argv[]) {
    if (argc != 2) {
        printf("There is must be file name.\n");
        return 1;
    }
    printf("c File %s\n", argv[1]);
    ifstream file(argv[1]);
    solve(file);

    return EXIT_SUCCESS;
}
